\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $x$:Id, $T$:Type, ${\it ks}$:(Knd List),\+
\\[0ex]${\it tr}$:($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$)\} $\rightarrow$decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$$T$$\rightarrow$$T$).
\-\\[0ex]fpf{-}compatible(Id; $x$.Type; id{-}deq; ${\it ds}$; fpf{-}single($x$; $T$))
\\[0ex]$\Rightarrow$ normal{-}type\=\{i:l\}\+
\\[0ex]($T$)
\-\\[0ex]$\Rightarrow$ ($\forall$$k$:Knd. ($k$ $\in$ ${\it ks}$) $\Rightarrow$ ($\uparrow$isrcv($k$)) $\Rightarrow$ ($i$ = destination(lnk($k$))))
\\[0ex]$\Rightarrow$ normal{-}ds\=\{i:l\}\+
\\[0ex](${\it ds}$)
\-\\[0ex]$\Rightarrow$ normal{-}da\=\{i:l\}\+
\\[0ex](${\it da}$)
\-\\[0ex]$\Rightarrow$ R{-}realizes\=\{i:l\}\+
\\[0ex](\=R{-}state{-}var($i$; ${\it ds}$; ${\it da}$; $x$; $T$; ${\it ks}$; ${\it tr}$);\+
\\[0ex]${\it es}$.(es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)
\\[0ex]$\Rightarrow$ \=(subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); $T$)\+
\\[0ex]c$\wedge$ \=(($\uparrow$bor(($\neg_{b}$null(${\it ks}$)); es{-}isconst(${\it es}$; $i$; $x$)))\+
\\[0ex]$\Rightarrow$ alle{-}at(\=${\it es}$;\+
\\[0ex]$i$;
\\[0ex]$e$.$\forall$${\it e'}$$\geq$$e$.\=es{-}after(${\it es}$; $x$; ${\it e'}$)\+
\\[0ex]=
\\[0ex]es{-}trans{-}state{-}from\{i:l\}(\=${\it es}$;${\it ks}$;\+
\\[0ex]${\it tr}$;es{-}when(${\it es}$; $x$; $e$);$e$;${\it e'}$)
\-\\[0ex]$\in$ $T$)))))
\-\-\-\-\-\-
\end{tabbing}